2018-12-29

Кубики

Меня просили написать две статьи: одну — обзор на новый кубик от JetBrains, Arend, а вторую для канала Формальная Философия. Поскольку кубики напрямую касаются формальной философии, я решил объединить, и дать не только обозрение на Arend, но и на все кубики.

Если предыдущая статья была об имплементации N2O на все языки, то эта статья будет об имплементации базовой библиотеки Групоид Инфинити на все кубические тайпчекеры. Пока их не много, но их количество стремительно увеличивается. В этом месяце мне посчастливилось портировать код Выпуска 1. Встраивание MLTT в тайп чекер, на новый прувер Arend от JetBrains.

Виды кубиков

Кубиками будем называть тайпчекеры которые реализуют кубическую теорию типов. Я главным образом определяю кубики по Воеводскому, как систему с двумя лямбдами. Если добавить в кубик линейные типы, получится система с тремя лямбдами. Систему со скольки лямбдами вы можете придумать? Спектральная лямбда-система?

Начнём с описания всех пяти флейворов кубических имплементаций. Тут в генеалогии прослеживается две главные ветки, одна берет свое начало от пейпера BCH¹, который формально давал вычислительную модель CCHM², имплементированную в Хаскеле как cubicaltt. Вторая линия — это декартовая кубическая теория, которя была опубликована в ABCFHL³ и AFH⁴ пейперах, и мплементирована как RedPRL (SML), redtt (OCaml), yacctt (Haskell), и Arend (Java).

1. cubicaltt: \(i: I)->, i @ x, сomp, /\, \/, ~, Glue, glue, unglue;
2. yacctt: \(i: I)->, i @ x, hcom, coe, V, Vin, Vproj;
3. Arend, redtt, RedPRL: \(i: I)->, i @ x, coe, V, Vin, Vproj;
4. hcomptrans: \(i: I)->, i @ 0, /\, \/, ~, hcomp, Glue, glue, unglue;
5. Agda: \(i: I)->, i @ x, hcomp, comp, \/, /\, ~, coe, Glue, glue, unglue.

Хотя это официальные пейперы современных кубиков (по сути — руководства в авторских математических синтаксисах), хочу сказать, что идею моделирования омега-групоидов Т-комплеками высказывали Браун и Хиггинс в 1981 году — BH⁵. Рональд Браун даже разработал свою систему обозначений с соединениями, которая описана в презентации A homotopical approach to algebraic topology via compositions of cubes, в этих слайдах также есть ссылка на работу Брауна, Хиггинса, Сиверы по некоммутативной алгебраической топологии.

Вообще нарезать пространство можно не обязательно кубами, для этого подойдет любой плотный узор из однотипных геометрических объектов. Например, пространство можно заполнить рисинками-бананами, или причудливыми трехмерными розетками.

Отличительные особенности

Декартовая модель кубической теории основанна не на примитивах композишина и склеек comp Glue glue, а на коершинах и гомогенных композициях coe, hcom а вместо glue — V-типы (в yacct две иерархии вселенных: претипы и типы Кана). Хотя и то и другое — операции Кана, последняя модель позволяет получить более компактные доказательства и более компактный тайпчекер.

Примеры

Как вы уже должны были прочитать из пейперов, кубическая теория типов выражается в терминах предпучков как функтор: F : ☐^op → Set, где ☐ — это Теория Лавира алгебр де Моргана, которые включеют в себя главным образом i /\ j, i \/ j, а также 1 - i, можно считать это дополнительными операциями на отрезке. Вообще алгебра Де Моргана это дистрибутивная решётка оснащённая контравариантной инволюцией, т.е. отображением ¬ : D^op → D таким, что ¬ ¬ A = A.

Для примера покажем как соединения /\, \/ выражаются через декартовые примитивы coe (Харпер) и hcomp (Мортберг). Первый примитив, coe, позволяет ужать ядро до минимума, имея лишь coe не нужно конекшинов и даже hcomp (но тогда HIT рекурсивные работать не будут). Второй более гибкий, и на нём основана ветка hcomptrans, единственная в которой чекаются расслоения Хопфа (ну и в Агде еще как порте cubicaltt модели).

cubicaltt/Agda

Синтаксис кубика настолько простой, что его BNF нотацию я могу привести на 16 строчек, следите за руками:


   sys := [ sides ]              side := (id=0)->exp+(id=1)->exp
  form := form\/f1+f1+f2        sides := #empty+cos+side
   cos := side,side+side,cos      mod := module id where imps dec
    f1 := f1/\f2                   f2 := -f2+id+0+1
   imp := import id               brs := #empty+cobrs
   app := exp exp                 tel := #empty+cotel
  imps := #list imp             cotel := (exp:exp) tel
    id := #list #nat              dec := #empty+codec
    u2 := glue+unglue+Glue         u1 := fill+comp
   ids := #list id                 br := ids->exp+ids@ids->exp
 codec := def dec
 cobrs := | br brs
   sum := #empty+id tel+id tel|sum+id tel < ids > sys
   def := data id tel=sum+id tel:exp=exp+id tel:exp where def
   exp := cotel*exp+cotel->exp+exp$\rightarrow$exp+(exp)+id
          (exp,exp)+\cotele->exp+split cobrs+exp.1+exp.2+
          exp+exp@form+app+u2 exp exp sys+u1 exp sys

В нем кроме индуктивных типов, которые расширены равенствами нет больше ничего, даже сплиты обязательно в том же порядке указывать, нет рекордов, зато есть сигма встроенная в ядро, так что ета-эквалити работает автоматически для пар. Будем считать cubicaltt самым референсным и минималистичным из всех.

С точки зрения cubicaltt мы всегда рассматриваем /\, \/ как аксиомамы, ведь доказывать с помощью них удобно, и первое что доказывается с помощью соединения — это стягиваемость синглтонов и через нее J. Мы же в этой статье попытаемся записать соединения через другие примитивы, так это аксиомы только в кубике:


 connectionOr (A: U) (a b: A) (p: Path A a b)
   : PathP (<x> Path A (p @ x) b) p (<_> b)
   = <y x> p @ (x \/ y)

Тут показана просто синонимическая типизация примитивов \/ и /\.


 connectionAnd (A: U) (a b: A) (p: Path A a b)
   : PathP (<x> Path A a (p @ x)) (<_> a) p
   = <x y> p @ (x /\ y)

Так как кубическая система типов Агды была портом из cubicaltt и Мортберг является офиицальным мейнтейнером либы agda/cubical, то в ней соединения тоже являются аксиомами.

Arend

Итак о синтаксисе Аренда. Аренд проделал на мой взгляд хирургическую адаптацию синтакиса кубика. Диапазон имен идентификаторов здесь расширен до агдового, добавились такие удобные штуки, как infix нотация, экстенсибл рекорды, которые есть только в Lean, тайп классы как расширения рекордов и их синонимы, вообщем все сделано очень приятно. Доволен потому, что когда я портировал категорную библиотеку на Аренд, мне пришлось применить парочку регекспов и файл чекнулся автоматом. Такая близость в генеалогии к классическому минималистическому кубику мне очень понравилась.

Arend открывает мир в мечты о формальной верификации Java или Kotlin программ. Скажем если взять Arend программы, стирать из них гомотопические доказатесльтва и экстрактить в чистую лямбду или Kotlin, то можно построить неплохой замкнутый формальный стек на отдельно взятой платформе JVM.

Да, можно говорить, что это все далеко от практики, но прототипы есть на других платфомах. Примеры существующих формальных стеков с I/O: ircbot IRC-бот для Lean, github.com/o29 для Coq с экстрактом в OCaml, и возможно даже линковкой с MirageOS. Хотя кубики все же ближе к инструменту математика, чем к инструменту верификации ПО, но рано или поздно я уверен появятся гомотопические замкнутые стеки с экстрактом до Haskell, хотя бы, спот уже есть: github.com/o4 для Agda с экстрактом в Haskell через компилятор MAlonzo.

Тут покажем как выразить их через coe (используется синтаксис Arend). В раннем Arend пейпере meet называется squeeze.


 \func meet (i j : I)
   => \let | p1 => \lam i j =>
                   (coe (\lam x => left = x) (path (\lam _ => left)) j @ i)
           | p2 => (path (\lam _ => path (\lam _ => left)))
       \in coe (\lam i => Path (\lam j => left = p1 i j) (path (\lam _ => left))
               (path (\lam j => p1 i j))) p2 right @ i @ j

 \func connAnd {A : \Type} {a b : A} (p : a = b) (i : I) : a = p @ i
   => path (\lam j => p @ meet i j)

yacctt/RedPRL

Чекер yacctt Мортберг имплементировал чтобы показать действие системы типов RedPRL в своем синтаксисе cubicaltt, который я дал формально в виде BNF выше.


 connAnd (A : U) (a b : A) (p : Path A a b) :
   PathP (<i> Path A a (p @ i)) (<_> a) p =
   <i j> hcom 0->1 A
   [ (i=0) -> <k> hcom 1->0 A [ (k=0) -> <_> a, (k=1) -> p ] (p @ k)
   , (i=1) -> <k> hcom 1->j A [ (k=0) -> <_> a, (k=1) -> p ] (p @ k)
   , (j=0) -> <k> hcom 1->0 A [ (k=0) -> <_> a, (k=1) -> p ] (p @ k)
   , (j=1) -> <k> hcom 1->i A [ (k=0) -> <_> a, (k=1) -> p ] (p @ k)
   ] a

Что мы можем сказать смотря на такой код? Во-первых мы можем сказать что в этой системе типов код поддается роботизации, а значит хорошо подходит для перебора и автомаического поиска пруфтермов.


 theorem Connection/And(#l:lvl) : (-> [ty : (U #l hcom)] [a b : ty]
         [p : (path [_] ty a b)] (path [i] (path [_] ty a (@ p i)) (abs [_] a) p))
    by { lam ty a b p => abs i j => `(hcom 0~>1 ty a
         [i=0 [k] (hcom 1~>0 ty (@ p k) [k=0 [_] a] [k=1 [l] (@ p l)])]
         [i=1 [k] (hcom 1~>j ty (@ p k) [k=0 [_] a] [k=1 [l] (@ p l)])]
         [j=0 [k] (hcom 1~>0 ty (@ p k) [k=0 [_] a] [k=1 [l] (@ p l)])]
         [j=1 [k] (hcom 1~>i ty (@ p k) [k=0 [_] a] [k=1 [l] (@ p l)])]
         [i=j [k] (hcom 1~>i ty (@ p k) [k=0 [_] a] [k=1 [l] (@ p l)])]) }.

redtt

Чекер redtt является реимплементаций ядра RedPRL с более современным и человеческим синтаксисом. А вот так выглядит имплементация конекшинов на прувере redtt, через comp. Тут в стиле AUTOMATH для более крутой лямбды используется []. Читайте статью про лямбда синтаксисы.


 def connection/and
     (A : type)
     (p : 𝕀 → A)
   : [i j] A [ | j=0 | i=0 → p 0 | j=1 → p i | i=1 → p j | i=j → p i ]
   = λ i j → let face (l k : 𝕀) : A = comp 0 l (p 0) [ | k=0 → refl | k=1 → p ]
  in comp 0 1 (p 0) [ | i=0 | j=0 → refl
                      | i=1 → face j | j=1 → face i | i=j → face i ]

Lean

В этом месяце сразу две большие новости. Первая — вливание кубической базовой библиотек Ground Zero в Groupoid Infinity, построенную путем прямого встраивания индуктивного отрезка и фактортипов в систему типов Lean (где фактортипы поддерживаются на вычислительном уровне, работает индукция). Вторая — стремительное начало Agda порта.


 def interval_cube : ℕ → Type
     | 0 := I
     | (n + 1) := interval_cube n × I

 def construct_cube {α : Sort u} :
     Π {n : ℕ}, (interval_cube n → α) → binary α n
     | 0 f := binary.leaf (f i₀) (f i₁)
     | (n + 1) f := binary.node (construct_cube (λ n, f ⟨n, i₀⟩))
                                (construct_cube (λ n, f ⟨n, i₁⟩))

 inductive Cube {α : Sort u} (n : ℕ) : binary α n → Type u
     | lam (f : interval_cube n → α) : Cube (construct_cube f)

 def Path {α : Sort u} (a b : α) := Cube 0 (binary.leaf a b)
 def Path.lam {α : Sort u} (f : I → α) : Path (f i₀) (f i₁) := Cube.lam f
 abbreviation lineP (σ : 𝕀 → Sort u) := Π (i : 𝕀), σ i

 notation `<` binder `> ` r:(scoped P, Path.lam P) := r

 def conn_and {α : Sort u} {a b : α} (p : a ⇝ b) :
     LineP (λ i, a ⇝ p # i) := λ i, <j> p # i ∧ j

Эпилог

Так как вы уже знаете чем отличаются все кубики, можете поставить звезду нашей библиотеке Групоид Инфинити, написанной на вашем любимом кубическом прувере. Мы собрали для вас агрегатор всех библиотек тут: https://cubical.systems.

Статус:

— cubicaltt — 5521 LOC — 492K
— Agda — 1330 LOC — 208K
— Lean — 1514 LOC — 112K
— Arend — 232 LOC — 11K

Литература: [1]. M.Bezem, T.Coquand, S.Huber. A model of type theory in cubical sets. [2]. C.Cohen, T.Coquand, S.Huber, A.Mörtberg. Cubical Type Theory: a constructive interpretation of the univalence axiom. [3]. C.Angiuli, G.Brunerie, T.Coquand, K.-B.Hou (Favonia), R.Harper, D.R.Licata. Cartesian Cubical Type Theory. [4]. C.Angiuli, K.-B.Hou (Favonia), R.Harper. Cartesian Cubical Computational Type Theory: Constructive Reasoning with Paths and Equalities. [5]. R.Brown, P.J.Higgins. The equivalence of ω-groupoids and cubical T-complexes.